\begin{tabbing}
SESAxioms\{i:l\}($E$;$T$;${\it pred?}$;${\it info}$;${\it when}$;${\it after}$;${\it time}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$, $l$:IdLnk.\+\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex]($\forall$${\it e''}$:$E$.
\\[0ex]($\uparrow$rcv?(${\it e''}$))
\\[0ex]$\Rightarrow$ (sender(${\it e''}$) = $e$)
\\[0ex]$\Rightarrow$ (link(${\it e''}$) = $l$)
\\[0ex]$\Rightarrow$ (((${\it e''}$ = ${\it e'}$) $\vee$ ${\it e''}$ $<$ ${\it e'}$) \& loc(${\it e'}$) = destination($l$))))
\-\-\\[0ex]\& (\=(($\forall$$e$, ${\it e'}$:$E$. (loc($e$) = loc(${\it e'}$)) $\Rightarrow$ (${\it pred?}$($e$) = ${\it pred?}$(${\it e'}$)) $\Rightarrow$ ($e$ = ${\it e'}$))\+
\\[0ex]\& SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]\& ($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ (loc(pred($e$)) = loc($e$)))
\\[0ex]\& ($\forall$$e$:$E$. ($\uparrow$rcv?($e$)) $\Rightarrow$ (loc(sender($e$)) = source(link($e$))))
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:$E$.\+
\\[0ex]($\uparrow$rcv?($e$))
\\[0ex]$\Rightarrow$ ($\uparrow$rcv?(${\it e'}$))
\\[0ex]$\Rightarrow$ (link($e$) = link(${\it e'}$))
\\[0ex]$\Rightarrow$ sender($e$) $<$ sender(${\it e'}$)
\\[0ex]$\Rightarrow$ $e$ $<$ ${\it e'}$))
\-\\[0ex]c$\wedge$ \=($\forall$$e$:$E$.\+
\\[0ex]($\neg$($\uparrow$first($e$)))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Id, $t$:$\mathbb{Q}$.\+
\\[0ex]${\it when}$($x$,$e$,$t$) = ${\it after}$($x$,pred($e$),$t$ + ((${\it time}$($e$)) {-} (${\it time}$(pred($e$))))))))
\-\-\-\-
\end{tabbing}